M1, M2:MsgA. M1  M2  (a:Id. a declared in M1  a declared in M2) 

latex

Definitions	x:A. B(x), P  Q, a declared in M, t.1, t.2, t  T, x. t(x), MsgA, M1  M2, Valtype(da;k), A c B, P & Q, f  g, x(s),
Lemmas	locl wf, assert wf, fpf-dom wf, Knd wf, Kind-deq wf, fpf-trivial-subtype-top, Id wf, ma-sub wf, msga wf